#include <sys/unistd.h>
#include<algorithm>
#include "Test2-SAT.h"
#include "2-SAT.h"
const int NUMBER_OF_TESTS = 20;
const int MAX = 20;
const int HUGE_MAX = INT_MAX / 1000000;
const int HUGE_NUMBER_OF_TESTS = 10;

inline std::vector<Lexem> MakeRandomExpression(int variables_number){
    int lexems_number = rand() % (variables_number * 7/2);
    //constant 7/2 provides us approximately equal number of solvable and unsolvable expressions generation.
    //experimentally checked
    std::vector<Lexem> expression;
    for(int lexem = 0; lexem < lexems_number; lexem++){
        int first =  rand() % variables_number;
        int second = rand() % variables_number;
        bool first_true = rand() % 2;
        bool second_true = rand() % 2;
        Lexem new_lexem(first, second, first_true,second_true);
        expression.push_back(new_lexem);
    }
    return expression;
}
bool IfGivenValuesFit(std::vector<bool> values, std::vector<Lexem> expression){
    for(int lexem = 0; lexem < expression.size();lexem++){
            bool first, second;
            if(expression[lexem].is_first_true){
                first = values[expression[lexem].first_variable];
            }
            else{
                first = !values[expression[lexem].first_variable];
            }
            if(expression[lexem].is_second_true){
                second = values[expression[lexem].second_variable];
            }
            else{
                second = !values[expression[lexem].second_variable];
            }
            if(!first && !second){
                return false;
            }
    }
    return true;
}
bool found_solution;
bool StupidIfSolutionExists(int variables_number, std::vector<Lexem> expression, int step, std::vector<bool> &values){
    if(found_solution) return true;
    if(step == variables_number){
        if( IfGivenValuesFit(values, expression)){
            found_solution = true;
            return true;
        }
        else return false;
    }
    else{
        values[step] = true;
        bool result1 = StupidIfSolutionExists( variables_number,  expression,  step + 1,  values);
        if(found_solution) return true;
        values[step] = false;
        bool result2 = StupidIfSolutionExists( variables_number,  expression,  step + 1,  values);
        if(found_solution) return true;
        return false;
    }
}

bool StupidIfSolutionExists(int variables_number, std::vector<Lexem> expression){
    found_solution = false;
    std::vector<bool> values(variables_number);
    return StupidIfSolutionExists(variables_number, expression, 0, values);
}

void Test2SAT(int variable_number, std::vector<Lexem> expression){
    std::vector<bool> solution_for_2sat = FindSolutionFor2SAT(variable_number, expression);
    if((solution_for_2sat.size() != 0) != (StupidIfSolutionExists(variable_number, expression))){
        throw std::logic_error("2-SAT ERROR : wrong answer about existance of solution");
    }
    if(solution_for_2sat.size() != 0){
        for(int lexem = 0; lexem < expression.size(); lexem++){
            if(!IfGivenValuesFit(solution_for_2sat, expression)){
                throw std::logic_error("2-SAT ERROR : wrong values");
            }
        }
    }
}
void Test2SAT(){
    for(int test = 0; test < NUMBER_OF_TESTS; test++){
        int variable_number = rand() % MAX + 1;
        std::vector<Lexem> expression = MakeRandomExpression(variable_number);
        Test2SAT(variable_number, expression);
    }
}


void TestMakeGraphFor2Sat(){
    for(int test = 0; test < NUMBER_OF_TESTS; test++){
        int variables_number = rand() % MAX + 1;
        std::vector<Lexem> expression = MakeRandomExpression(variables_number);
        std::auto_ptr<Graph> graph = MakeGraphFor2SAT(expression, variables_number);
        std::set<edge> got_edges;
        for(int vertex = 0; vertex < graph->GetNumberOfVertices(); vertex++){
            std::set<int> incidence_list = graph->GetIncidentList(vertex);
            for(std::set<int>::iterator incident_vertex = incidence_list.begin(); incident_vertex != incidence_list.end(); incident_vertex++){
                edge new_edge (vertex, *incident_vertex);
                got_edges.insert(new_edge);
            }
        }
        std::set<edge> right_edges;
        for(int lexem = 0; lexem < expression.size(); lexem++){
            int from,to;
            if(expression[lexem].is_first_true){
                from = expression[lexem].first_variable * 2 ;
            }
            else{
                from = expression[lexem].first_variable * 2 + 1;
            }
            if(!expression[lexem].is_second_true){
                to = expression[lexem].second_variable * 2;
            }
            else{
                to = expression[lexem].second_variable * 2 + 1;
            }
            edge new_edge(from,to);
            right_edges.insert(new_edge);
            if(!expression[lexem].is_first_true){
                to = expression[lexem].first_variable * 2;
            } 
            else{
                to = expression[lexem].first_variable * 2 + 1;
            }
            if(expression[lexem].is_second_true){
                from = expression[lexem].second_variable * 2;
            }
            else{
                from = expression[lexem].second_variable * 2 + 1;
            }
            new_edge = edge(from,to);
            right_edges.insert(new_edge);
        }
        if(right_edges != got_edges){
            throw std::logic_error("MakeGraphFor2SAT ERROR : wrong edges");
        }
    }
}


void GenerateAllExpressions(int variables_number, int step, std::vector<Lexem> &expression){
    if(step == 4 * variables_number * variables_number){
        Test2SAT(variables_number, expression);
    }
    else{
        GenerateAllExpressions(variables_number, step + 1, expression);
        int code = step;
        bool is_first_true = code % 2;
        code /= 2;
        bool is_second_true = code % 2;
        code /= 2;
        int first = code % variables_number;
        int second = code / variables_number;
        Lexem lexem (first, second, is_first_true, is_second_true);
        expression.push_back(lexem);
        GenerateAllExpressions(variables_number, step + 1, expression);
    }
}
void Test2SATOnSmallTests(){
    std::vector<Lexem> expression;
    GenerateAllExpressions(1, 0, expression);
    expression.clear();
    GenerateAllExpressions(2, 0, expression);
    expression.clear();
    GenerateAllExpressions(3, 0, expression);
}


void Test2SATOnHugeTests(){
    for(int test = 0; test < HUGE_NUMBER_OF_TESTS; test++){
        int variables_number = rand() % HUGE_MAX;
        std::vector<Lexem> expression = MakeRandomExpression(variables_number);
        bool no_solution = FindSolutionFor2SAT(variables_number, expression).size() == 0;
        std::vector<int> shuffle(variables_number);
        for(int variable = 0; variable < shuffle.size(); variable++){
            shuffle[variable] = variable;
        }
        std::random_shuffle(shuffle.begin(), shuffle.end());
        for(int lexem = 0; lexem < expression.size(); lexem++){
            int first = shuffle[expression[lexem].first_variable];
            int second = shuffle[expression[lexem].second_variable];
            Lexem new_lexem (first, second, expression[lexem].is_first_true, expression[lexem].is_second_true);
            expression[lexem] = new_lexem;
        }
        bool no_solution_shuffe = FindSolutionFor2SAT(variables_number, expression).size() == 0;
        if(no_solution != no_solution_shuffe){
            throw std::logic_error("FindSolutionFor2SAT ERROR : wrong answer about existance of solution");
        }
    }
}
void TestAll2SAT(){
    Test2SAT();
    TestMakeGraphFor2Sat();
   // Test2SATOnSmallTests();
    //commented because it works very slowly. There are 2^16 expressions on 2 variables, so, if you reaaly want to test 
    //algorithm on all this expressions, uncomment it.
    Test2SATOnHugeTests();
}















